|
|
Analysis of C Programs with Dynamic Linked Data Structures
Šoková, Veronika ; Rogalewicz, Adam (referee) ; Vojnar, Tomáš (advisor)
This master's thesis deals with the analysis of dynamic linked data structures using shape analysis used in the Predator tool. It describes the chosen abstract domain for heap representation - symbolic memory graphs. It deals with the design of framework for the development of static analyzers based on Clang/LLVM. The main contribution is implementing and testing LLVM's transformation passes that simplify the LLVM IR. Second contribution is the optimization of parameters for parallel run of several variants of the Predator tool. Parameters are tuned for benchmark from SV-COMP'16, where our tool won gold medal in Heap Data Structures category. Last contribution is the design of verification core with the focus on the SMG domain.
|
|
|
Automata in Infinite-state Formal Verification
Lengál, Ondřej ; Jančar, Petr (referee) ; Veith, Helmut (referee) ; Esparza, Javier (referee) ; Vojnar, Tomáš (advisor)
Tato práce se zaměřuje na konečné automaty nad konečnými slovy a konečnými stromy, a použití těchto automatů při formální verifikaci nekonečně stavových systémů. Práce se nejdříve věnuje rozšíření existujícího přístupu pro verifikaci programů které manipulují s haldou (konkrétně programů s dynamickými datovými strukturami), jenž je založen na stromových automatech. V práci je navrženo několik rozšíření tohoto přístupu, jako například jeho plná automatizace či jeho rozšíření o podporu uspořádaných dat. V práci jsou popsány nové rozhodovací procedury pro dvě logiky, které jsou často používány ve formální verifikaci: pro separační logiku a pro slabou monadickou druhořádovou logiku s následníkem. Obě tyto rozhodovací procedury jsou založeny na převodu jejich problému do automatové domény a následné manipulaci v této cílové doméně. Posledním přínosem této práce je vývoj nových algoritmů k efektivní manipulaci se stromovými automaty, s důrazem na testování inkluze jazyků těchto automatů a manipulaci s automaty s velkými abecedami, a implementace těchto algoritmů v knihovně pro obecné použití. Tyto vyvinuté algoritmy jsou použity jako klíčová technologie, která umožňuje použití výše uvedených technik v praxi.
|
|
|
Creation of Database and Classification of Diatoms
Svoboda, Jan ; Nötzel, Ralf (referee) ; Drahanský, Martin (advisor)
Výsledná aplikace pracuje s vytvořenou databází, obsahující obrázky jednotlivých rozsivek a informace o nich uložené v XML dokumentu. Nad touto databází jsou zajištěny základní operace přidávání, úpravy, mazání a vyhledávání. Vyhledávání může probíhat třemi způsoby, a to pomocí textových vstupů, obrázkových vstupů nebo jejich kombinací. Algoritmus vyhledávání pomocí obrázkových vstupů se snaží najít v databázi co nejpodobnější kandidáty s ohledem na tvar a tloušťku schránky rozsivky a na vnitřní strukturu rozsivky jako takové. Toto vyhledávání je nejčastěji znepřesněno kvalitou pořízených snímků, či obrázků porovnávaných rozsivek. Program obsahuje přehledné a intuitivní grafické rozhraní, jež nám pohodlně umožňuje prohlížet stávající databázi a provádět operace nad ní s možností nastavení filtrovacích hodnot při vyhledávání.
|
|
|
Automation of Exoscopic Analysis Using Image Processing of Sedimentary Grains Acquired by Electron Microscope
Křupka, Aleš ; Křížek,, Marek (referee) ; Baroňák, Ivan (referee) ; Říha, Kamil (advisor)
This thesis deals with image analysis methods which can be exploited in exoscopic analysis of sedimentary grains, specifically for the purpose of distinguishing between geomorphologic geneses which influenced a form of sedimentary grains. The images of sedimentary grains were acquired by a scanning electron microscope. The main contribution is the proposal of multiple methods that can significantly automate the exoscopic analysis. These methods cover the automatic segmentation of grains in image, the automatic analysis of roundness of 2D grain projection and the classification of geomorphologic geneses according to the grain surface structure. In the section concerning the automatic segmentation, a segmentation method enabling an easy subsequent manual result correction was proposed. This method is based on the split-and-merge approach. The individual steps the procedure were designed to exploit specific properties of sedimentary grain images in order to obtain the best segmentation results. In the section concerning the automatic roundness analysis of 2D projection of sedimentary grains, an influence of pixel resolution on a result roundness value was evaluated. Further, a minimal number of grains, which is necessary to analyze in order to reliably compare a pair of geomorphological geneses, was investigated. For the determination of this number, a method was proposed and experimentally verified. In the section of automatic analysis of sedimentary grain surface structure, a method for classification of geomorphologic geneses was proposed. The method utilizes low-level texture features which describes individual images of sedimentary grains. A model of geomorphological genesis is constituted of a set of histograms representing occurrences of different configurations of low-level texture features. The methods proposed in the thesis were tested and evaluated based on a database, which consists of sedimentary grain samples from 4 different geomorphological geneses (eolic, glacial, slope and volcanic).
|
|
|
Automata in Decision Procedures and Performance Analysis
Fiedor, Tomáš ; Barnat, Jiří (referee) ; Radu, Iosif (referee) ; Vojnar, Tomáš (advisor)
Tato práce se věnuje vylepšení současného stavu formalní analýzy a verifikace založené na automatech a zaměřené na systémy s nekonečnými stavovými prostory. V první části se práce zabývá dvěma rozhodovacími procedurami pro logiku WS1S, které jsou založené na korespondenci mezi formulemi logiky WS1S a konečnými automaty. První metoda je založena na tzv. antiřetězcích, ale, je limitována pouze na formule v prenexním normálním tvaru. Následně je tento přístup zobecněn na libovolné formule, jsou zavedeny tzv. jazykové termy a na jejich základě je navržena nová procedura, která pracuje za běhu a zpracovává tyto termy "líným" způsobem. Abychom získali efektivní rozhodovací proceduru, je dále navržena sada optimalizací (přičemž některé nejsou limitovány pouze pro naše přístupy). Obě metody jsou srovnány s ostatními nástroji implementujícími různé známé rozhodovací procedury. Získané výsledky jsou povzbuzující a ukazují, že použitelnost logiky WS1S je možno rozšířit na širší třídu formulí. V druhé části se práce zabývá analýzou mezí zdrojů programů manipulujících s haldou. Je zde navržena nová třída tzv. tvarových norem založených na délkách cest mezi význačnými místy na haldě, které jsou automaticky odvozovány z analyzovaného programu. Na základě této třídy norem je dále navržen kalkul, který je schopen přesně odvodit změny odvozených normů a použít je k vygenerování odpovídající celočíselné reprezentace vstupního programu, která je následně využita pro následovanou dedikovanou analýzou mezí zdrojů. Tato metoda byla implementována nad analýzou tvaru založenou na tzv. lesních automatech, implementovanou v nástroji Forester, a dále byl použit dobře zavedený analyzátor mezí zdrojů, implementovaný v nástroji Loopus. V experimentální evaluaci bylo ukázáno, že je opravdu takto získán silný analyzátor, který je schopen odvodit meze programů, které ještě nikdy plně automatizovaně odvozené nebyly.
|
|
|
Geometric morphometrics of shape and symmetry of flower structures - ecological and evolutionary significance
Rubešová, Veronika ; Neustupa, Jiří (advisor) ; Woodard, Kateřina (referee)
I did a research of relevant literature on geometric morphometrics, its usage for a study of floral symmetry, and ecological and evolutionary significance of floral symmetry in general. Description and application of morphometric methods is included in the first part of the thesis. Then, the main types of floral symmetries are described and illustrated. Morphometric studies on several model floral lineages are discussed in subsequent parts of this bachelor thesis. Many of the studies are made on some species of family Brassicaceae. Modern morphometric methods and perspectives of their application in floral research are presented in the last chapter.
|
|
|
Automata in Decision Procedures and Performance Analysis
Fiedor, Tomáš ; Barnat, Jiří (referee) ; Radu, Iosif (referee) ; Vojnar, Tomáš (advisor)
Tato práce se věnuje vylepšení současného stavu formalní analýzy a verifikace založené na automatech a zaměřené na systémy s nekonečnými stavovými prostory. V první části se práce zabývá dvěma rozhodovacími procedurami pro logiku WS1S, které jsou založené na korespondenci mezi formulemi logiky WS1S a konečnými automaty. První metoda je založena na tzv. antiřetězcích, ale, je limitována pouze na formule v prenexním normálním tvaru. Následně je tento přístup zobecněn na libovolné formule, jsou zavedeny tzv. jazykové termy a na jejich základě je navržena nová procedura, která pracuje za běhu a zpracovává tyto termy "líným" způsobem. Abychom získali efektivní rozhodovací proceduru, je dále navržena sada optimalizací (přičemž některé nejsou limitovány pouze pro naše přístupy). Obě metody jsou srovnány s ostatními nástroji implementujícími různé známé rozhodovací procedury. Získané výsledky jsou povzbuzující a ukazují, že použitelnost logiky WS1S je možno rozšířit na širší třídu formulí. V druhé části se práce zabývá analýzou mezí zdrojů programů manipulujících s haldou. Je zde navržena nová třída tzv. tvarových norem založených na délkách cest mezi význačnými místy na haldě, které jsou automaticky odvozovány z analyzovaného programu. Na základě této třídy norem je dále navržen kalkul, který je schopen přesně odvodit změny odvozených normů a použít je k vygenerování odpovídající celočíselné reprezentace vstupního programu, která je následně využita pro následovanou dedikovanou analýzou mezí zdrojů. Tato metoda byla implementována nad analýzou tvaru založenou na tzv. lesních automatech, implementovanou v nástroji Forester, a dále byl použit dobře zavedený analyzátor mezí zdrojů, implementovaný v nástroji Loopus. V experimentální evaluaci bylo ukázáno, že je opravdu takto získán silný analyzátor, který je schopen odvodit meze programů, které ještě nikdy plně automatizovaně odvozené nebyly.
|
|
|
Surface registrations for topology transfer in geometric morphometry
Dupej, Ján ; Pelikán, Josef (advisor) ; Telea, Alexandru C. (referee) ; Váša, Libor (referee)
Geometric morphometry serves biologists and anthropologists to rigorously and quantitatively describe shapes. These representations can be treated as a statistical sample, allowing the researchers to study its variability within groups and correlate it to other features. Geometric morphometry uses landmarks as the proxy for shape, with consistent semantics in each specimen. General triangle meshes do not have this property, and as such, semantically consistent remeshes must be created artificially. This thesis deals with the design of an algorithm that consistently resamples a set of surface models for the purpose of statistical analysis. Coherent point drift was employed to perform nonrigid registration, whose result is then used to generate a semantically consistent remeshes. This approach was successfully applied in a number of studies. As CPD is compute-intensive, we propose methods of accelerating both its initialization and processing phases. Also, an extension was introduced, that can map the deviation of the surfaces from perfect bilateral symmetry and analyze it in a sample, which is significant, among others, for quantification of pathologies. Manual trimming of the surfaces and merging datasets results in outlier regions in the individual surfaces and potentially large differences in their vertex...
|
|
|
Geometric morphometrics of shape and symmetry of flower structures - ecological and evolutionary significance
Rubešová, Veronika ; Neustupa, Jiří (advisor) ; Woodard, Kateřina (referee)
I did a research of relevant literature on geometric morphometrics, its usage for a study of floral symmetry, and ecological and evolutionary significance of floral symmetry in general. Description and application of morphometric methods is included in the first part of the thesis. Then, the main types of floral symmetries are described and illustrated. Morphometric studies on several model floral lineages are discussed in subsequent parts of this bachelor thesis. Many of the studies are made on some species of family Brassicaceae. Modern morphometric methods and perspectives of their application in floral research are presented in the last chapter.
|
|
|
Correspondence Problem in Geometrics Morphometric Tasks
Krajíček, Václav ; Pelikán, Josef (advisor) ; Kosinka, Jiří (referee) ; Sochor, Jiří (referee)
Title: Correspondence Problem in Geometric Morphometrics Tasks Author: Václav Krajíček Department / Institute: Department of Software and Computer Science Education Supervisor of the doctoral thesis: RNDr. Josef Pelikán Supervisor's e-mail address: pepca@cgg.mff.cuni.cz Abstract: Shape analysis in physical anthropology, biomedicine, and related disci- plines is mostly done using landmarks or by measuring distances. New techno- logical advancements allow the digitization of object's appearance in the form of triangular meshes or volume images. These digital images are especially beneficial in the cases when landmarks cannot be used to effectively describe the shape. In order to statistically analyze shape in a sample of observations, which are represented by these modalities, correspondence has to be found. Registration is a crucial tool in mapping the shape representations into a common space where correspondence is found by nearest neighbor principle in the case of triangular meshes or by overlaps in the case of volume images. B- spline based non-rigid registration is chosen because of its versatility, relative speed and ability to handle both meshes and volume images. Experiments were also performed with other alternatives - Thin-plate splines and Coherent point drift. The algorithm was modified to handle...
|
guest ::
